(set-logic QF_BV)
(declare-fun _substvar_52_ () (_ BitVec 8))
(declare-fun _substvar_54_ () (_ BitVec 32))
(declare-fun _substvar_50_ () (_ BitVec 32))
(declare-fun _substvar_44_ () (_ BitVec 8))
(declare-fun _substvar_45_ () (_ BitVec 32))
(declare-fun _substvar_47_ () (_ BitVec 32))
(assert (= _substvar_45_ ((_ sign_extend 24) _substvar_44_)))
(assert (= _substvar_47_ _substvar_45_))
(assert (= _substvar_50_ _substvar_47_))
(assert (= _substvar_52_ ((_ extract 7 0) _substvar_50_)))
(assert (= _substvar_54_ ((_ sign_extend 24) _substvar_52_)))
(assert (= (_ bv0 32) (bvadd _substvar_54_ ((_ extract 31 0) (_ bv24 64)))))
(check-sat)
(exit)
